es:ES, A, B:Type, Ia:AbsInterface(A), Ib, Ic:AbsInterface(B), f1:(E(Ia)B).
(glued(es; B; f1; Ia; Ib) & glued(es; B; (e.Ib(e)); Ib; Ic))  glued(es; B; f1; Ia; Ic) 

latex

Definitions

t  T, x:A. B(x), AbsInterface(A), x:AB(x), E(X), glued(es; B; f; Ia; Ib), x:A  B(x), P & Q, P  Q, Type, ES, b, glues(es; B; g; f; Ia; Ib), Top, Void, x:A.B(x), <a, b>, s = t, left + right, EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), f(a), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), let x,y = A in B(x;y), E, True, T, SqStable(P), {x:A| B(x)} , x:A. B(x), t.1, X(e), , A c B, x.A(x), {T}, s ~ t, SQType(T), f o g

Lemmas

compose wf, glued wf, es-E-interface wf, es-interface-val wf, sq stable from decidable, decidable assert, subtype rel function, subtype rel sum, glued-composes, es-interface wf